Nuprl Lemma : fseg_weakening
11,40
postcript
pdf
T
:Type,
l1
,
l2
:(
T
List). (
l1
=
l2
)
fseg(
T
;
l1
;
l2
)
latex
ProofTree
Definitions
t
T
,
s
=
t
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
as
@
bs
,
,
type
List
,
Type
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
fseg(
T
;
L1
;
L2
)
,
[]
Lemmas
append
wf
origin
T:Type, l1, l2:(T List). (l1 = l2) 
fseg(T;l1;l2)
T:Type, l1, l2:(T List). (l1 = l2) fseg(T;l1;l2)
T
B(x)x:A. B(x)
B(x)
x:A. B(x) Q